A:Realizer. R-Feasible(A)  A || A 

latex

Definitions

x:A. B(x), P  Q, A || B, t  T, Prop, Y, if b t else f fi, P & Q, True, true, false, x. t(x), AB, A, False, ij, R-Feasible(R), , , Unit, P  Q, P  Q, {T}, x(s), , S  T,

Lemmas

nat wf, R-size wf, nat plus inc, nat plus wf, R-Feasible wf, es realizer wf, le wf, Rplus? wf, bool wf, eqtt to assert, Rplus-implies, R-size-decreases, R-compat-Rplus2, Rplus-left wf, Rplus-right wf, R-compat-symmetry, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Rnone? wf, eq id wf, R-loc wf, Id wf, assert-eq-id, fpf-compatible-self, id-deq wf, Rds wf, Knd wf, Kind-deq wf, Rda wf, eq bd wf, R-base-domain wf, R-frame-compat-self, not functionality wrt iff, R-interface-compat-self, nat properties, ge wf